Automated Theorem Provers, such as Lean, offer a way to rigorously guarantee the correctness of theorems or software. This offers a way to verifying quantum cryptographic protocols, compilers, or more abstract theorems. I'll discuss the state of an ongoing effort to develop this and the challenges ahead.
Speaker's Bio
Alex Meiburg is a postdoc at Perimeter Institute and University of Waterloo. His interests lie at the intersection of quantum information and complexity theory, with an eye towards AI as an aid for improving the process along the way.